f:(). (n:. ((f(n))))  {((f(mu(f)))) & (i:. (i < mu(f))  (((f(i)))))} 

latex

Definitions	x:A. B(x), P  Q, x:A. B(x), P & Q, {T}, mu(f), t  T, Y, if b then t else f fi , tt, ff, , A  B, A, False, i  j , SQType(T), , T, True, , Unit, P  Q, Dec(P), P  Q,
Lemmas	nat wf, bool wf, eqtt to assert, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, le wf, nat properties, ge wf, decidable int equal, squash wf, true wf, mu wf